    {-# LANGUAGE NondecreasingIndentation #-}

    {-# OPTIONS_GHC -fno-warn-orphans #-}

    -- | Rewriting with arbitrary rules.
    --
    --   The user specifies a relation symbol by the pragma
    --   @
    --       {-\# BUILTIN REWRITE rel \#-}
    --   @
    --   where @rel@ should be of type @Δ → (lhs rhs : A) → Set i@.
    --
    --   Then the user can add rewrite rules by the pragma
    --   @
    --       {-\# REWRITE q \#-}
    --   @
    --   where @q@ should be a closed term of type @Γ → rel us lhs rhs@.
    --
    --   We then intend to add a rewrite rule
    --   @
    --       Γ ⊢ lhs ↦ rhs : B
    --   @
    --   to the signature where @B = A[us/Δ]@.
    --
    --   To this end, we normalize @lhs@, which should be of the form
    --   @
    --       f ts
    --   @
    --   for a @'Def'@-symbol f (postulate, function, data, record, constructor).
    --   Further, @FV(ts) = dom(Γ)@.
    --   The rule @q :: Γ ⊢ f ts ↦ rhs : B@ is added to the signature
    --   to the definition of @f@.
    --
    --   When reducing a term @Ψ ⊢ f vs@ is stuck, we try the rewrites for @f@,
    --   by trying to unify @vs@ with @ts@.
    --   This is for now done by substituting fresh metas Xs for the bound
    --   variables in @ts@ and checking equality with @vs@
    --   @
    --       Ψ ⊢ (f ts)[Xs/Γ] = f vs : B[Xs/Γ]
    --   @
    --   If successful (no open metas/constraints), we replace @f vs@ by
    --   @rhs[Xs/Γ]@ and continue reducing.

    module Agda.TypeChecking.Rewriting where

    import Prelude hiding (null)

    import Control.Monad.Trans.Maybe ( MaybeT(..), runMaybeT )

    import Data.Either (partitionEithers)
    import Data.Foldable (toList)
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Agda.Interaction.Options

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Internal.Pattern

    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Conversion
    import qualified Agda.TypeChecking.Positivity.Occurrence as Pos
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Rewriting.Confluence
    import Agda.TypeChecking.Rewriting.NonLinMatch
    import Agda.TypeChecking.Rewriting.NonLinPattern
    import Agda.TypeChecking.Warnings

    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Utils.Set1 as Set1
    import Agda.Utils.Size
    import qualified Agda.Utils.SmallSet as SmallSet

    import Agda.Utils.Impossible
    import Agda.Utils.Either

    requireOptionRewriting :: TCM ()
    requireOptionRewriting :: TCM ()
    requireOptionRewriting =
      TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (PragmaOptions -> Bool
    optRewriting (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    NeedOptionRewriting

    -- | Check that the name given to the BUILTIN REWRITE is actually
    --   a relation symbol.
    --   I.e., its type should be of the form @Δ → (lhs : A) (rhs : B) → Set ℓ@.
    --   Note: we do not care about hiding/non-hiding of lhs and rhs.
    verifyBuiltinRewrite :: Term -> Type -> TCM ()
    verifyBuiltinRewrite :: Term -> Type -> TCM ()
    verifyBuiltinRewrite Term
    v Type
    t = do
      TCM ()
    requireOptionRewriting
      TCMT IO (Maybe RelView) -> TCM () -> (RelView -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Type -> TCMT IO (Maybe RelView)
    relView Type
    t)
        (TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> IncorrectTypeForRewriteRelationReason -> TypeError
    IncorrectTypeForRewriteRelation Term
    v IncorrectTypeForRewriteRelationReason
    ShouldAcceptAtLeastTwoArguments) ((RelView -> TCM ()) -> TCM ()) -> (RelView -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        \ (RelView Tele (Dom Type)
    tel [Dom (ArgName, Type)]
    delta Dom Type
    a Dom Type
    b Type
    core) -> do
        Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Type
    a Bool -> Bool -> Bool
    && Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Type
    b) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> IncorrectTypeForRewriteRelationReason -> TypeError
    IncorrectTypeForRewriteRelation Term
    v IncorrectTypeForRewriteRelationReason
    FinalTwoArgumentsNotVisible
        case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    core of
          Sort{}   -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Con{}    -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Level{}  -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lam{}    -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Pi{}     -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> IncorrectTypeForRewriteRelationReason -> TypeError
    IncorrectTypeForRewriteRelation Term
    v (Type -> Tele (Dom Type) -> IncorrectTypeForRewriteRelationReason
    TypeDoesNotEndInSort Type
    core Tele (Dom Type)
    tel)

    -- | Deconstructing a type into @Δ → t → t' → core@.
    data RelView = RelView
      { RelView -> Tele (Dom Type)
    relViewTel   :: Telescope  -- ^ The whole telescope @Δ, t, t'@.
      , RelView -> [Dom (ArgName, Type)]
    relViewDelta :: ListTel    -- ^ @Δ@.
      , RelView -> Dom Type
    relViewType  :: Dom Type   -- ^ @t@.
      , RelView -> Dom Type
    relViewType' :: Dom Type   -- ^ @t'@.
      , RelView -> Type
    relViewCore  :: Type       -- ^ @core@.
      }

    -- | Deconstructing a type into @Δ → t → t' → core@.
    --   Returns @Nothing@ if not enough argument types.
    relView :: Type -> TCM (Maybe RelView)
    relView :: Type -> TCMT IO (Maybe RelView)
    relView Type
    t = do
      TelV tel core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
      let n                = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
          (delta, lastTwo) = splitAt (n - 2) $ telToList tel
      if size lastTwo < 2 then return Nothing else do
        let [a, b] = fmap snd <$> lastTwo
        return $ Just $ RelView tel delta a b core

    -- | Check the given rewrite rules and add them to the signature.
    addRewriteRules :: [QName] -> TCM ()
    addRewriteRules :: [QName] -> TCM ()
    addRewriteRules [QName]
    qs = do

      -- Check the rewrite rules
      rews <- (QName -> TCMT IO (Maybe RewriteRule))
    -> [QName] -> TCMT IO RewriteRules
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m (Maybe b)) -> [a] -> m [b]
    mapMaybeM QName -> TCMT IO (Maybe RewriteRule)
    checkRewriteRule [QName]
    qs

      -- Add rewrite rules to the signature
      forM_ rews $ \RewriteRule
    rew -> do
        let f :: QName
    f = RewriteRule -> QName
    rewHead RewriteRule
    rew
            matchables :: [QName]
    matchables = RewriteRule -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables RewriteRule
    rew
        ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "adding rule" 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 (RewriteRule -> QName
    rewName RewriteRule
    rew) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
          TCMT IO Doc
    "to the definition of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f
        ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "matchable symbols: " 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]
    matchables
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> RewriteRules -> [QName] -> Signature -> Signature
    addRewriteRulesFor QName
    f [RewriteRule
    rew] [QName]
    matchables

      -- Run confluence check for the new rules
      -- (should be done after adding all rules, see #3795)
      whenJustM (optConfluenceCheck <$> pragmaOptions) $ \ConfluenceCheck
    confChk -> do
        -- Warn if --cubical is enabled
        TCMT IO (Maybe Cubical) -> (Cubical -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption ((Cubical -> TCM ()) -> TCM ()) -> (Cubical -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \Cubical
    _ -> Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning Warning
    ConfluenceForCubicalNotSupported
        -- Global confluence checker requires rules to be sorted
        -- according to the generality of their lhs
        Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (ConfluenceCheck
    confChk ConfluenceCheck -> ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck
    GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [QName] -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ((QName -> QName) -> [QName] -> [QName]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn QName -> QName
    forall a. a -> a
    id ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ (RewriteRule -> QName) -> RewriteRules -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map RewriteRule -> QName
    rewHead RewriteRules
    rews) QName -> TCM ()
    sortRulesOfSymbol
        ConfluenceCheck -> RewriteRules -> TCM ()
    checkConfluenceOfRules ConfluenceCheck
    confChk RewriteRules
    rews
        ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "done checking confluence of rules" 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((RewriteRule -> TCMT IO Doc) -> RewriteRules -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (QName -> TCMT IO Doc)
    -> (RewriteRule -> QName) -> RewriteRule -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> QName
    rewName) RewriteRules
    rews)

    -- Auxiliary function for checkRewriteRule.
    -- | Get domain of rewrite relation.
    rewriteRelationDom :: QName -> TCM (ListTel, Dom Type)
    rewriteRelationDom :: QName -> TCM ([Dom (ArgName, Type)], Dom Type)
    rewriteRelationDom QName
    rel = do
      -- We know that the type of rel is that of a relation.
      relV <- Type -> TCMT IO (Maybe RelView)
    relView (Type -> TCMT IO (Maybe RelView))
    -> TCMT IO Type -> TCMT IO (Maybe RelView)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    rel
      let RelView _tel delta a _a' _core = fromMaybe __IMPOSSIBLE__ relV
      reportSDoc "rewriting" 30 $ do
        "rewrite relation at type " <+> do
          inTopContext $ prettyTCM (telFromList delta) <+> " |- " <+> do
            addContext delta $ prettyTCM a
      return (delta, a)

    -- | Check the validity of @q : Γ → rel us lhs rhs@ as rewrite rule
    --   @
    --       Γ ⊢ lhs ↦ rhs : B
    --   @
    --   where @B = A[us/Δ]@.
    --   Remember that @rel : Δ → A → A → Set i@, so
    --   @rel us : (lhs rhs : A[us/Δ]) → Set i@.
    --   Returns the checked rewrite rule to be added to the signature.
    checkRewriteRule :: QName -> TCM (Maybe RewriteRule)
    checkRewriteRule :: QName -> TCMT IO (Maybe RewriteRule)
    checkRewriteRule QName
    q = MaybeT (TCMT IO) RewriteRule -> TCMT IO (Maybe RewriteRule)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) RewriteRule -> TCMT IO (Maybe RewriteRule))
    -> MaybeT (TCMT IO) RewriteRule -> TCMT IO (Maybe RewriteRule)
    forall a b. (a -> b) -> a -> b
    $ QName
    -> MaybeT (TCMT IO) RewriteRule -> MaybeT (TCMT IO) RewriteRule
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange QName
    q do
      TCM () -> MaybeT (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM ()
    requireOptionRewriting
      rels <- TCMT IO (Set QName) -> MaybeT (TCMT IO) (Set QName)
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO (Set QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    m (Set QName)
    getBuiltinRewriteRelations
      reportSDoc "rewriting.relations" 40 $ vcat
        [ "Rewrite relations:"
        , prettyList $ map prettyTCM $ toList rels
        ]
      def <- instantiateDef =<< getConstInfo q
      -- Issue 1651: Check that we are not adding a rewrite rule
      -- for a type signature whose body has not been type-checked yet.
      when (isEmptyFunction $ theDef def) $
        illegalRule BeforeFunctionDefinition
      -- Issue 6643: Also check that there are no mututal definitions
      -- that are not yet defined.
      whenJustM (asksTC envMutualBlock) \ MutualId
    mb -> do
        qs <- MutualBlock -> Set QName
    mutualNames (MutualBlock -> Set QName)
    -> MaybeT (TCMT IO) MutualBlock -> MaybeT (TCMT IO) (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualId -> MaybeT (TCMT IO) MutualBlock
    forall (tcm :: * -> *).
    ReadTCState tcm =>
    MutualId -> tcm MutualBlock
    lookupMutualBlock MutualId
    mb
        when (Set.member q qs) $ forM_ qs $ \QName
    r -> do
          MaybeT (TCMT IO) Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Defn -> Bool
    isEmptyFunction (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Bool)
    -> MaybeT (TCMT IO) Definition -> MaybeT (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> MaybeT (TCMT IO) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    r) (MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ())
    -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
            IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> IllegalRewriteRuleReason
    BeforeMutualFunctionDefinition QName
    r

      -- Get rewrite rule (type of q).
      TelV gamma1 core <- telView $ defType def
      reportSDoc "rewriting" 30 $ vcat
        [ "attempting to add rewrite rule of type "
        , prettyTCM gamma1
        , " |- " <+> do addContext gamma1 $ prettyTCM core
        ]
      let failureBlocked :: Blocker -> MaybeT TCM a
          failureBlocked Blocker
    b
            | Set1.IsNonEmpty NESet MetaId
    ms <- Blocker -> Set MetaId
    allBlockingMetas    Blocker
    b = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ NESet MetaId -> IllegalRewriteRuleReason
    ContainsUnsolvedMetaVariables NESet MetaId
    ms
            | Set1.IsNonEmpty NESet ProblemId
    ps <- Blocker -> Set ProblemId
    allBlockingProblems Blocker
    b = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ NESet ProblemId -> IllegalRewriteRuleReason
    BlockedOnProblems NESet ProblemId
    ps
            | Set1.IsNonEmpty NESet QName
    qs <- Blocker -> Set QName
    allBlockingDefs     Blocker
    b = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ NESet QName -> IllegalRewriteRuleReason
    RequiresDefinitions NESet QName
    qs
            | Bool
    otherwise = MaybeT (TCMT IO) a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      let failureFreeVars :: IntSet -> MaybeT TCM a
          failureFreeVars IntSet
    xs = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ IntSet -> IllegalRewriteRuleReason
    VariablesNotBoundByLHS IntSet
    xs
      let failureNonLinearPars :: IntSet -> MaybeT TCM a
          failureNonLinearPars IntSet
    xs = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ IntSet -> IllegalRewriteRuleReason
    VariablesBoundMoreThanOnce IntSet
    xs

      -- Check that type of q targets rel.
      case unEl core of
        Def QName
    rel es :: Elims
    es@(Elim' Term
    _:Elim' Term
    _:Elims
    _) | QName
    rel QName -> Set QName -> Bool
    forall a. Eq a => a -> Set a -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Set QName
    rels -> do
          (delta, a) <- TCM ([Dom (ArgName, Type)], Dom Type)
    -> MaybeT (TCMT IO) ([Dom (ArgName, Type)], Dom Type)
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM ([Dom (ArgName, Type)], Dom Type)
     -> MaybeT (TCMT IO) ([Dom (ArgName, Type)], Dom Type))
    -> TCM ([Dom (ArgName, Type)], Dom Type)
    -> MaybeT (TCMT IO) ([Dom (ArgName, Type)], Dom Type)
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM ([Dom (ArgName, Type)], Dom Type)
    rewriteRelationDom QName
    rel
          -- Because of the type of rel (Γ → sort), all es are applications.
          let vs = (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
          -- The last two arguments are lhs and rhs.
              n  = [Term] -> Int
    forall a. Sized a => a -> Int
    size [Term]
    vs
              (us, [lhs, rhs]) = splitAt (n - 2) vs
          unless (size delta == size us) __IMPOSSIBLE__
          lhs <- instantiateFull lhs
          rhs <- instantiateFull rhs
          b   <- instantiateFull $ applySubst (parallelS $ reverse us) a

          gamma0 <- getContextTelescope
          gamma1 <- instantiateFull gamma1
          let gamma = Tele (Dom Type)
    gamma0 Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    `abstract` Tele (Dom Type)
    gamma1

          -- 2017-06-18, Jesper: Unfold inlined definitions on the LHS.
          -- This is necessary to replace copies created by imports by their
          -- original definition.
          lhs <- modifyAllowedReductions (const $ SmallSet.singleton InlineReductions) $ reduce lhs

          -- Find head symbol f of the lhs, its type, its parameters (in case of a constructor), and its arguments.
          (f , hd , t , pars , es) <- case lhs of
            Def QName
    f Elims
    es -> do
              def <- QName -> MaybeT (TCMT IO) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
              checkAxFunOrCon f def
              return (f , Def f , defType def , [] , es)
            Con ConHead
    c ConInfo
    ci Elims
    vs -> do
              let hd :: Elims -> Term
    hd = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci
              ~(Just ((_ , _ , pars) , t)) <- ConHead
    -> Type
    -> MaybeT (TCMT IO) (Maybe ((QName, Type, [Arg Term]), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
    getFullyAppliedConType ConHead
    c (Type
     -> MaybeT (TCMT IO) (Maybe ((QName, Type, [Arg Term]), Type)))
    -> Type
    -> MaybeT (TCMT IO) (Maybe ((QName, Type, [Arg Term]), Type))
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    b
              pars <- addContext gamma1 $ checkParametersAreGeneral c pars
              return (conName c , hd , t , pars , vs)
            Term
    _ -> do
              ArgName -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting.rule.check" Int
    30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
    -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
                [ TCMT IO Doc
    "LHSNotDefinitionOrConstructor: ", Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    lhs ]
              IllegalRewriteRuleReason
    -> MaybeT (TCMT IO) (QName, Elims -> Term, Type, [Int], Elims)
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule IllegalRewriteRuleReason
    LHSNotDefinitionOrConstructor

          ifNotAlreadyAdded f $ do

          addContext gamma1 $ do

            checkNoLhsReduction f hd es

            ps <- fromRightM failureBlocked $ lift $
              catchPatternErr (pure . Left) $
                Right <$> patternFrom relevant 0 (t , Def f) es

            reportSDoc "rewriting" 30 $
              "Pattern generated from lhs: " <+> prettyTCM (PDef f ps)

            -- We need to check two properties on the variables used in the rewrite rule
            -- 1. For actually being able to apply the rewrite rule, we need
            --    that all variables that occur in the rule (on the left or the right)
            --    are bound in a pattern position on the left.
            -- 2. To preserve soundness, we need that all the variables that are used
            --    in the *proof* of the rewrite rule are bound in the lhs.
            --    For rewrite rules on constructors, we consider parameters to be bound
            --    even though they don't appear in the lhs, since they can be reconstructed.
            --    For postulated or abstract rewrite rules, we consider all arguments
            --    as 'used' (see #5238).
            let boundVars = PElims -> IntSet
    forall a. NLPatVars a => a -> IntSet
    nlPatVars PElims
    ps
                freeVars  = (PElims, Term) -> IntSet
    forall t. Free t => t -> IntSet
    allFreeVars (PElims
    ps,Term
    rhs)
                allVars   = [Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    gamma
                usedVars  = case Definition -> Defn
    theDef Definition
    def of
                  Function{}         -> Definition -> IntSet
    usedArgs Definition
    def
                  Axiom{}            -> IntSet
    allVars
                  AbstractDefn{}     -> IntSet
    allVars
                  Constructor{}      -> IntSet
    allVars
                  Primitive{}        -> IntSet
    allVars
                  DataOrRecSig{}     -> IntSet
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  GeneralizableVar{} -> IntSet
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  Datatype{}         -> IntSet
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  Record{}           -> IntSet
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  PrimitiveSort{}    -> IntSet
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            reportSDoc "rewriting" 70 $
              "variables bound by the pattern: " <+> text (show boundVars)
            reportSDoc "rewriting" 70 $
              "variables free in the rewrite rule: " <+> text (show freeVars)
            reportSDoc "rewriting" 70 $
              "variables used by the rewrite rule: " <+> text (show usedVars)
            unlessNull (freeVars IntSet.\\ boundVars) failureFreeVars
            unlessNull (usedVars IntSet.\\ (boundVars `IntSet.union` IntSet.fromList pars)) failureFreeVars

            reportSDoc "rewriting" 70 $
              "variables bound in (erased) parameter position: " <+> text (show pars)
            unlessNull (boundVars `IntSet.intersection` IntSet.fromList pars) failureNonLinearPars

            top <- fromMaybe __IMPOSSIBLE__ <$> currentTopLevelModule
            let rew = QName
    -> Tele (Dom Type)
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> TopLevelModuleName
    -> RewriteRule
    RewriteRule QName
    q Tele (Dom Type)
    gamma QName
    f PElims
    ps Term
    rhs (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    b) Bool
    False TopLevelModuleName
    top

            reportSDoc "rewriting" 10 $ vcat
              [ "checked rewrite rule" , prettyTCM rew ]
            reportSDoc "rewriting" 90 $ vcat
              [ "checked rewrite rule" , text (show rew) ]

            return rew

        Term
    _ -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) RewriteRule
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule IllegalRewriteRuleReason
    DoesNotTargetRewriteRelation

      where
        illegalRule :: IllegalRewriteRuleReason -> MaybeT TCM a
        illegalRule :: forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule IllegalRewriteRuleReason
    reason = do
          TCM () -> MaybeT (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> MaybeT (TCMT IO) ()) -> TCM () -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> IllegalRewriteRuleReason -> Warning
    IllegalRewriteRule QName
    q IllegalRewriteRuleReason
    reason
          MaybeT (TCMT IO) a
    forall a. MaybeT (TCMT IO) a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> MaybeT TCM ()
        checkNoLhsReduction :: QName -> (Elims -> Term) -> Elims -> MaybeT (TCMT IO) ()
    checkNoLhsReduction QName
    f Elims -> Term
    hd Elims
    es = do
          -- Skip this check when global confluence check is enabled, as
          -- redundant rewrite rules may be required to prove confluence.
          MaybeT (TCMT IO) Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM ((Maybe ConfluenceCheck -> Maybe ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck -> Maybe ConfluenceCheck
    forall a. a -> Maybe a
    Just ConfluenceCheck
    GlobalConfluenceCheck) (Maybe ConfluenceCheck -> Bool)
    -> (PragmaOptions -> Maybe ConfluenceCheck)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck (PragmaOptions -> Bool)
    -> MaybeT (TCMT IO) PragmaOptions -> MaybeT (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (TCMT IO) PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ())
    -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ do
          let v :: Term
    v = Elims -> Term
    hd Elims
    es
          v' <- Term -> MaybeT (TCMT IO) Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
          let fail :: MaybeT TCM a
              fail = do
                ArgName -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    20 (TCMT IO Doc -> MaybeT (TCMT IO) ())
    -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "v  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Term -> ArgName
    forall a. Show a => a -> ArgName
    show Term
    v)
                ArgName -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "rewriting" Int
    20 (TCMT IO Doc -> MaybeT (TCMT IO) ())
    -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "v' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Term -> ArgName
    forall a. Show a => a -> ArgName
    show Term
    v')
                IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> IllegalRewriteRuleReason
    LHSReduces Term
    v Term
    v'
          es' <- case v' of
            Def QName
    f' Elims
    es'   | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f'         -> Elims -> MaybeT (TCMT IO) Elims
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elims
    es'
            Con ConHead
    c' ConInfo
    _ Elims
    es' | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead -> QName
    conName ConHead
    c' -> Elims -> MaybeT (TCMT IO) Elims
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elims
    es'
            Term
    _                              -> MaybeT (TCMT IO) Elims
    forall a. MaybeT (TCMT IO) a
    fail
          unless (null es && null es') $ do
            a   <- lift $ computeElimHeadType f es es'
            pol <- getPolarity' CmpEq f
            ok  <- lift $ dontAssignMetas $ tryConversion $
                     compareElims pol [] a (Def f []) es es'
            unless ok fail

        checkAxFunOrCon :: QName -> Definition -> MaybeT TCM ()
        checkAxFunOrCon :: QName -> Definition -> MaybeT (TCMT IO) ()
    checkAxFunOrCon QName
    f Definition
    def = case Definition -> Defn
    theDef Definition
    def of
          Axiom{}        -> () -> MaybeT (TCMT IO) ()
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          def :: Defn
    def@Function{} -> do
            Maybe Projection
    -> (Projection -> MaybeT (TCMT IO) ()) -> MaybeT (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Either ProjectionLikenessMissing Projection -> Maybe Projection
    forall a b. Either a b -> Maybe b
    maybeRight (Defn -> Either ProjectionLikenessMissing Projection
    funProjection Defn
    def)) ((Projection -> MaybeT (TCMT IO) ()) -> MaybeT (TCMT IO) ())
    -> (Projection -> MaybeT (TCMT IO) ()) -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ \Projection
    proj -> case Projection -> Maybe QName
    projProper Projection
    proj of
              Maybe QName
    Nothing -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> IllegalRewriteRuleReason
    HeadSymbolIsProjectionLikeFunction QName
    f
              Just{} -> MaybeT (TCMT IO) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                -- Andreas, 2024-08-20
                -- A projection ought to be impossible in the head, since they are represented
                -- in post-fix in the internal syntax.
                -- Thus, a lone projection @p@ will be @λ x → x .p@
                -- and an applied projection @p t@ will be @t .p@.
            MaybeT (TCMT IO) Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Maybe ConfluenceCheck -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe ConfluenceCheck -> Bool)
    -> (PragmaOptions -> Maybe ConfluenceCheck)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck (PragmaOptions -> Bool)
    -> MaybeT (TCMT IO) PragmaOptions -> MaybeT (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (TCMT IO) PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ())
    -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ do
              let simpleClause :: Clause -> (Elims, Maybe Term)
    simpleClause Clause
    cl = ([NamedArg DeBruijnPattern] -> Elims
    patternsToElims (Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl) , Clause -> Maybe Term
    clauseBody Clause
    cl)
              cls <- [(Elims, Maybe Term)] -> MaybeT (TCMT IO) [(Elims, Maybe Term)]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull ([(Elims, Maybe Term)] -> MaybeT (TCMT IO) [(Elims, Maybe Term)])
    -> [(Elims, Maybe Term)] -> MaybeT (TCMT IO) [(Elims, Maybe Term)]
    forall a b. (a -> b) -> a -> b
    $ (Clause -> (Elims, Maybe Term))
    -> [Clause] -> [(Elims, Maybe Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> (Elims, Maybe Term)
    simpleClause ([Clause] -> [(Elims, Maybe Term)])
    -> [Clause] -> [(Elims, Maybe Term)]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Clause]
    funClauses Defn
    def
              unless (noMetas cls) $ illegalRule $ HeadSymbolContainsMetas f

          Constructor{}  -> () -> MaybeT (TCMT IO) ()
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          AbstractDefn{} -> () -> MaybeT (TCMT IO) ()
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Primitive{}    -> () -> MaybeT (TCMT IO) ()
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () -- TODO: is this fine?
          Datatype{}     -> MaybeT (TCMT IO) ()
    illegalHead
          Record{}       -> MaybeT (TCMT IO) ()
    illegalHead
          DatatypeDefn{} -> MaybeT (TCMT IO) ()
    illegalHead
          RecordDefn{}   -> MaybeT (TCMT IO) ()
    illegalHead
          DataOrRecSig{} -> MaybeT (TCMT IO) ()
    illegalHead
          PrimitiveSort{}-> MaybeT (TCMT IO) ()
    illegalHead
          GeneralizableVar{} -> MaybeT (TCMT IO) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          where
          illegalHead :: MaybeT (TCMT IO) ()
    illegalHead = IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) ())
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> IllegalRewriteRuleReason
    HeadSymbolIsTypeConstructor QName
    f

        ifNotAlreadyAdded :: QName -> MaybeT TCM RewriteRule -> MaybeT TCM RewriteRule
        ifNotAlreadyAdded :: QName
    -> MaybeT (TCMT IO) RewriteRule -> MaybeT (TCMT IO) RewriteRule
    ifNotAlreadyAdded QName
    f MaybeT (TCMT IO) RewriteRule
    cont = do
          rews <- QName -> MaybeT (TCMT IO) RewriteRules
    forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
    getRewriteRulesFor QName
    f
          -- check if q is already an added rewrite rule
          case List.find ((q ==) . rewName) rews of
            Just RewriteRule
    rew -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) RewriteRule
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule IllegalRewriteRuleReason
    DuplicateRewriteRule
            Maybe RewriteRule
    Nothing -> MaybeT (TCMT IO) RewriteRule
    cont

        usedArgs :: Definition -> IntSet
        usedArgs :: Definition -> IntSet
    usedArgs Definition
    def = [Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ ((Occurrence, Int) -> Int) -> [(Occurrence, Int)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Occurrence, Int) -> Int
    forall a b. (a, b) -> b
    snd ([(Occurrence, Int)] -> [Int]) -> [(Occurrence, Int)] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [(Occurrence, Int)]
    usedIxs
          where
            occs :: [Occurrence]
    occs = Definition -> [Occurrence]
    defArgOccurrences Definition
    def
            allIxs :: [(Occurrence, Int)]
    allIxs = [Occurrence] -> [Int] -> [(Occurrence, Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Occurrence]
    occs ([Int] -> [(Occurrence, Int)]) -> [Int] -> [(Occurrence, Int)]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Occurrence] -> Int
    forall a. Sized a => a -> Int
    size [Occurrence]
    occs
            usedIxs :: [(Occurrence, Int)]
    usedIxs = ((Occurrence, Int) -> Bool)
    -> [(Occurrence, Int)] -> [(Occurrence, Int)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Occurrence -> Bool
    used (Occurrence -> Bool)
    -> ((Occurrence, Int) -> Occurrence) -> (Occurrence, Int) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Occurrence, Int) -> Occurrence
    forall a b. (a, b) -> a
    fst) [(Occurrence, Int)]
    allIxs
            used :: Occurrence -> Bool
    used Occurrence
    Pos.Unused = Bool
    False
            used Occurrence
    _          = Bool
    True

        checkParametersAreGeneral :: ConHead -> Args -> MaybeT TCM [Int]
        checkParametersAreGeneral :: ConHead -> [Arg Term] -> MaybeT (TCMT IO) [Int]
    checkParametersAreGeneral ConHead
    c [Arg Term]
    vs = do
            is <- [Arg Term] -> MaybeT (TCMT IO) [Int]
    loop [Arg Term]
    vs
            unless (fastDistinct is) $ errorNotGeneral
            return is
          where
            loop :: [Arg Term] -> MaybeT (TCMT IO) [Int]
    loop []       = [Int] -> MaybeT (TCMT IO) [Int]
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            loop (Arg Term
    v : [Arg Term]
    vs) = case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v of
              Var Int
    i [] -> (Int
    i Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    :) ([Int] -> [Int])
    -> MaybeT (TCMT IO) [Int] -> MaybeT (TCMT IO) [Int]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Term] -> MaybeT (TCMT IO) [Int]
    loop [Arg Term]
    vs
              Term
    _        -> MaybeT (TCMT IO) [Int]
    forall a. MaybeT (TCMT IO) a
    errorNotGeneral

            errorNotGeneral :: MaybeT TCM a
            errorNotGeneral :: forall a. MaybeT (TCMT IO) a
    errorNotGeneral = IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a. IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    illegalRule (IllegalRewriteRuleReason -> MaybeT (TCMT IO) a)
    -> IllegalRewriteRuleReason -> MaybeT (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ ConHead -> [Arg Term] -> IllegalRewriteRuleReason
    ConstructorParametersNotGeneral ConHead
    c [Arg Term]
    vs

    -- | @rewriteWith t f es rew@ where @f : t@
    --   tries to rewrite @f es@ with @rew@, returning the reduct if successful.
    rewriteWith :: Type
                -> (Elims -> Term)
                -> RewriteRule
                -> Elims
                -> ReduceM (Either (Blocked Term) Term)
    rewriteWith :: Type
    -> (Elims -> Term)
    -> RewriteRule
    -> Elims
    -> ReduceM (Either (Blocked Term) Term)
    rewriteWith Type
    t Elims -> Term
    hd rew :: RewriteRule
    rew@(RewriteRule QName
    q Tele (Dom Type)
    gamma QName
    _ PElims
    ps Term
    rhs Type
    b Bool
    isClause TopLevelModuleName
    _) Elims
    es
     | Bool
    isClause = Either (Blocked Term) Term -> ReduceM (Either (Blocked Term) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Term) Term
     -> ReduceM (Either (Blocked Term) Term))
    -> Either (Blocked Term) Term
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Either (Blocked Term) Term
    forall a b. a -> Either a b
    Left (Blocked Term -> Either (Blocked Term) Term)
    -> Blocked Term -> Either (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> Term -> Blocked Term
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked (Term -> Blocked Term) -> Term -> Blocked Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hd Elims
    es
     | Bool
    otherwise = do
      ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    50 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ TCMT IO Doc
    "{ attempting to rewrite term " 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 (Elims -> Term
    hd Elims
    es)
        , TCMT IO Doc
    " having head " 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 (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
    " of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
        , TCMT IO Doc
    " with rule " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> RewriteRule -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => RewriteRule -> m Doc
    prettyTCM RewriteRule
    rew
        ]) (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
      ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    90 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ TCMT IO Doc
    "raw: attempting to rewrite term " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Term -> ArgName) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> ArgName
    forall a. Show a => a -> ArgName
    show) (Elims -> Term
    hd Elims
    es)
        , TCMT IO Doc
    " having head " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Term -> ArgName) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> ArgName
    forall a. Show a => a -> ArgName
    show) (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
    " of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Type -> ArgName) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> ArgName
    forall a. Show a => a -> ArgName
    show) Type
    t
        , TCMT IO Doc
    " with rule " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (RewriteRule -> ArgName) -> RewriteRule -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> ArgName
    forall a. Show a => a -> ArgName
    show) RewriteRule
    rew
        ]) (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
      result <- Tele (Dom Type)
    -> TypeOf Elims
    -> PElims
    -> Elims
    -> ReduceM (Either Blocked_ Substitution)
    forall (m :: * -> *) a b.
    (PureTCM m, Match a b) =>
    Tele (Dom Type)
    -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch Tele (Dom Type)
    gamma (Type
    t,Elims -> Term
    hd) PElims
    ps Elims
    es
      case result of
        Left Blocked_
    block -> ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    50 TCMT IO Doc
    "}" (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $
          Either (Blocked Term) Term -> ReduceM (Either (Blocked Term) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Term) Term
     -> ReduceM (Either (Blocked Term) Term))
    -> Either (Blocked Term) Term
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Either (Blocked Term) Term
    forall a b. a -> Either a b
    Left (Blocked Term -> Either (Blocked Term) Term)
    -> Blocked Term -> Either (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ Blocked_
    block Blocked_ -> Term -> Blocked Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Elims -> Term
    hd Elims
    es -- TODO: remember reductions
        Right Substitution
    sub  -> do
          let v' :: Term
    v' = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub Term
    rhs
          ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    50 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "rewrote " 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 (Elims -> Term
    hd Elims
    es)
            , TCMT IO Doc
    " to " 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' TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "}"
            ]) (ReduceM (Either (Blocked Term) Term)
     -> ReduceM (Either (Blocked Term) Term))
    -> ReduceM (Either (Blocked Term) Term)
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
          Either (Blocked Term) Term -> ReduceM (Either (Blocked Term) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Term) Term
     -> ReduceM (Either (Blocked Term) Term))
    -> Either (Blocked Term) Term
    -> ReduceM (Either (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Either (Blocked Term) Term
    forall a b. b -> Either a b
    Right Term
    v'

    -- | @rewrite b v rules es@ tries to rewrite @v@ applied to @es@ with the
    --   rewrite rules @rules@. @b@ is the default blocking tag.
    rewrite :: Blocked_ -> (Elims -> Term) -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
    rewrite :: Blocked_
    -> (Elims -> Term)
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    rewrite Blocked_
    block Elims -> Term
    hd RewriteRules
    rules Elims
    es = do
      rewritingAllowed <- PragmaOptions -> Bool
    optRewriting (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      if (rewritingAllowed && not (null rules)) then do
        (_ , t) <- fromMaybe __IMPOSSIBLE__ <$> getTypedHead (hd [])
        loop block t rules =<< instantiateFull' es -- TODO: remove instantiateFull?
      else
        return $ NoReduction (block $> hd es)
      where
        loop :: Blocked_ -> Type -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
        loop :: Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop Blocked_
    block Type
    t [] Elims
    es =
          ArgName
    -> Int
    -> TCMT IO Doc
    -> ReduceM (Reduced (Blocked Term) Term)
    -> ReduceM (Reduced (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "rewriting.rewrite" Int
    20 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "failed to rewrite " 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 (Elims -> Term
    hd Elims
    es)
            , TCMT IO Doc
    "blocking tag" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Blocked_ -> ArgName
    forall a. Show a => a -> ArgName
    show Blocked_
    block)
            ]) (ReduceM (Reduced (Blocked Term) Term)
     -> ReduceM (Reduced (Blocked Term) Term))
    -> ReduceM (Reduced (Blocked Term) Term)
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ do
          Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Term) Term
     -> ReduceM (Reduced (Blocked Term) Term))
    -> Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Reduced (Blocked Term) Term
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked Term -> Reduced (Blocked Term) Term)
    -> Blocked Term -> Reduced (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ Blocked_
    block Blocked_ -> Term -> Blocked Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Elims -> Term
    hd Elims
    es
        loop Blocked_
    block Type
    t (RewriteRule
    rew:RewriteRules
    rews) Elims
    es
         | let n :: Int
    n = RewriteRule -> Int
    rewArity RewriteRule
    rew, Elims -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Elims
    es Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n = do
              let (Elims
    es1, Elims
    es2) = Int -> Elims -> (Elims, Elims)
    forall i a. Integral i => i -> [a] -> ([a], [a])
    List.genericSplitAt Int
    n Elims
    es
              result <- Type
    -> (Elims -> Term)
    -> RewriteRule
    -> Elims
    -> ReduceM (Either (Blocked Term) Term)
    rewriteWith Type
    t Elims -> Term
    hd RewriteRule
    rew Elims
    es1
              case result of
                Left (Blocked Blocker
    m Term
    u)    -> Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop (Blocked_
    block Blocked_ -> Blocked_ -> Blocked_
    forall a. Monoid a => a -> a -> a
    `mappend` Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    m ()) Type
    t RewriteRules
    rews Elims
    es
                Left (NotBlocked NotBlocked' Term
    _ Term
    _) -> Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop Blocked_
    block Type
    t RewriteRules
    rews Elims
    es
                Right Term
    w               -> Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Term) Term
     -> ReduceM (Reduced (Blocked Term) Term))
    -> Reduced (Blocked Term) Term
    -> ReduceM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Simplification -> Term -> Reduced (Blocked Term) Term
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    YesSimplification (Term -> Reduced (Blocked Term) Term)
    -> Term -> Reduced (Blocked Term) Term
    forall a b. (a -> b) -> a -> b
    $ Term
    w Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es2
         | Bool
    otherwise = Blocked_
    -> Type
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    loop (Blocked_
    block Blocked_ -> Blocked_ -> Blocked_
    forall a. Monoid a => a -> a -> a
    `mappend` NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    Underapplied ()) Type
    t RewriteRules
    rews Elims
    es

        rewArity :: RewriteRule -> Int
        rewArity :: RewriteRule -> Int
    rewArity = PElims -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (PElims -> Int) -> (RewriteRule -> PElims) -> RewriteRule -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> PElims
    rewPats